https://roundtablelaw.medium.com/utterly-unpersuasive-formal-methods-and-law-bb8ecf048374Read more... )

Computer Aided Formal Reasoning, курс Торстена Альтенкриха, с кодом на Агде и справочными материалами по ней.

http://www.cs.toronto.edu/~hehner/FMSD/

Вроде, ничего. Даже довольно обширно.

Итак, в SQLite действительно 1100 строк кода тестов к одной строке кода: As of version 3.7.8 (all statistics in the report are against that release of SQLite), the SQLite library consists of approximately 77.6 KSLOC of C code. (KSLOC means thousands of "Source Lines Of Code" or, in other words, lines of code excluding blank lines and comments.) By ( Read more... )

Что меня ещё интересует ( Read more... )

antilamer интересный проект задумал: Легковесная верификация многопоточных программ.

Мои бывшие коллеги из ИТМиВТ применяли для таких вещей Alloy, с существенными результатами. Во-первых, переводя спецификацию ZigBee на Alloy, они выявили ошибки в стандарте. В некоторые поля из восьми бит предлагалось помещать значения от 0 до 65535. Во-вторых, когда они ( Read more... )

Спецификация устройств, на специальном ЯП под названием Жар-Птица Лирохвост.

В языке есть "монада" преобразования состояния, есть чистые функции, есть типы с размерностью.

Ровно то, что мы сделали для описания процессорных ядер, только в нашем случае это был Haskell.

http://lambda-the-ultimate.org/node/3858#comment-59775 - ссылка на комментарий одного из разработчиков seL4, формально верифицированного ядра, реализующего интерфейс L4 ( Read more... )

Experience report: using objective caml to develop safety-critical embedded tools in a certification framework (ACM).

Как народ кодогенератор для сертифицированного применения писал.

Слайды к докладу на ICFP.

Проект Ynot (почему бы и нет?, я так думаю).

Проект, что позволяет формализовать императивные вычисления. "На развороте" у них реляционная БД, без сохранения на диск (in-memory), со строгим доказательством правильности работы.

Что ещё хотел добавить.

Интересной задачей является формулирование в типах рекурсивной структуры вида struct list { int ( Read more... )